/* Benchmarks for the PionterC verifier. */

// alloc should always return a unique pointer

struct T 
{
  int car;
};

/*@ x->car==10*/
struct T* f(struct T* x)
{
  int b;
  struct T* y;
  y = alloc(struct T);
  y -> car = 9;
  return y;  
}
/*@ x->car ==10 */